COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.bb QUANTIFIERS AND ABSTRACT FORMS
C00008 ENDMK
C⊗;
.bb QUANTIFIERS AND ABSTRACT FORMS

	The object of this section is to introduce concepts formed
by quantification and description.  We start with a class of ⊗objects 
which we will call %2inner variables%1 and build up from them and
constants a class of %2abstract forms%1 using certain functions
with names like ⊗ttelephone and ⊗TTelepone.

	As far as the outer logic is concerned the %2inner variables%1
are objects and not variables at all, and therefore we will need
variables ranging over inner variables.  Furthermore the %2inner
variables%1 can either range over concepts or things.  To keep all this
straight we make the following typographical conventions:

1. As before,  an expression whose value is a concept begins in upper case and
one whose value is a thing is in lower case.

2. An %2inner variable%1 is represented by a doubled letter followed
by digits, and a variable ranging over %2abstract forms%1 is represented
by doubled letters without digits.  Thus  ⊗XX0 is an inner variable
ranging over concepts, and ⊗XX is a variable ranging over concept-valued
abstract forms.
Likewise ⊗xx0 is an inner variable representing things, and
⊗xx is a variable ranging thing-valued abstract forms.

	Inner variables are one kind of abstract form, and another kind
are constants.  Constants are treated similarly to variables.  Thus
we have ⊗MMike - a constant whose value is the concept represented
by ⊗Mike and ⊗mmike a constant whose value is Mike himself.

	Abstract forms are built from constants and variables by
functions.  Thus ⊗TTelephone takes an abstract form representing a
person into an abstract form representing his telephone number.
Thus we have %2TTelephone PP0%1 is an abstract form and so is
%2TTelephone MMike%1.  %2TTelephone PP%1 is an expression with a variable
⊗PP ranging over abstract forms.
Corresponding to all the functions of the previous sections we have
form making functions represented by doubling the initial letters.

	We have two additional ways of making abstract forms.  Namely,
if ⊗XX is an inner variable and ⊗QQ is an abstract form, then
⊗AAll(XX,QQ) is an abstract form and so is ⊗TThe(XX,QQ).
Thus %2TThe(PP0,KKnow(PP0,TTelephone MMike))%1 is an abstract form,
and we intend that it shall have as value a concept of the unique
person who knows Mike's telephone number.  In the logic ⊗AAll and
⊗TThe are functions.  In order to avoid trouble with bound variables,
we shall want

!!g50:	%2TThe(PP0,KKnow(PP0,TTelephone MMike)) = TThe(PP5,KKnow(PP5,TTelephone Mike))%1

	In order to go from concept-valued abstract forms to concepts,
we introduce two functions %2Value EE%1 and %2Value(EE,α)%1 where α
is called a state vector and assigns values to all inner variables.
If the abstract form ⊗EE has no inner variables, then %2Value EE%1
can be used.  The inner form %2TThe(PP0,KKnow(PP0,TTelephone MMike))%1
has no variables; the function ⊗TThe gets rid of the variable ⊗PP0 
in its second argument, so %2Value TThe(PP0,KKnow(PP0,TTelephone MMike))%1
is the concept of the unique person who knows Mike's telephone number.
If there is such a person, then
%2denote Value TThe(PP0,KKnow(PP0,TTelephone MMike))%1 is that person.

	Similarly,

!!g51:	%2Value AAll(PP0,KKnow(PP0,TTelephone MMike) Implies
KKnow(PP0,TTelephone MMary))%1

is the proposition that everyone who knows Mike's telephone number
also knows Mary's.

(If the reader is getting impatient with all this formalism, let him
remember that the above formulas are constants in a first order logic
formalism, i.e. are formed by applying functions to arguments.  This
will pay off later, I promise).

	Actually, we may have made more distinctions in the notation
than are necessary, but it is easier to remove them than add them later.